Library Tactics

Require Export PointsETC.
Require Export Rtools.
Require Export transformations.
Require Export ConwayPermutations.

Ltac unfold_all := unfold sa, sb, sc, s, SA, SB, SC, SW, SS, DeltaMaj, e, J, RR, r ,TauMaj.

Ltac normalize_conway_notations :=
 try rewrite <- Delta_perm_1; try rewrite <- Delta_perm_2;
 try rewrite <- J_perm_1; try rewrite <- J_perm_2;
 try rewrite <- e_perm_1; try rewrite <- e_perm_2;
 try rewrite <- RR_perm_1; try rewrite <- RR_perm_2;
 try rewrite <- SS_perm_1; try rewrite <- SS_perm_2;
 try rewrite <- r_perm_1; try rewrite <- r_perm_2.

Definition sqrt_n x := sqrt x.

Ltac normalize_all_sqrt := (repeat
 match goal with
 [ |- context[sqrt ?X] ] ⇒ replace (sqrt X) with (sqrt_n X) by trivial;(field_simplify (a+b+c) X)
 end);unfold sqrt_n.

Ltac normalize_all_sqrt_ring := (repeat
 match goal with
 [ |- context[sqrt ?X] ] ⇒ replace (sqrt X) with (sqrt_n X) by trivial;(ring_simplify (a+b+c) X)
 end);unfold sqrt_n.

Section Test.

Context `{M:triangle_theory}.

Goal sqrt ((a+b)^2) + sqrt(a+b) = sqrt(b+a)+sqrt (a^2+b^2+2×a×b).
Proof.
normalize_all_sqrt.
ring.
Qed.

End Test.

Ltac prepare_col := red;simpl.
Ltac prepare_field := normalize_conway_notations;unfold_all.
Ltac prepare_field_2 := normalize_conway_notations;unfold_all;normalize_all_sqrt.

Ltac myfield := field;repeat split;try assumption.

Ltac solve_eq_1 := prepare_field;myfield.
Ltac solve_eq_2 := prepare_field;apply Rminus_diag_uniq;field_simplify;[
repeat (rewrite sqrt_pow);[ myfield | ..]|..].
Ltac solve_eq_3 := prepare_field_2;apply Rminus_diag_uniq;field_simplify;[
repeat (rewrite sqrt_pow);[ myfield | ..]|..].

Ltac solve_eq := first [solve_eq_1 | solve_eq_2 | solve_eq_3 ].

Ltac solve_col := intros;prepare_col;solve_eq.


Ltac set_all_sqrt := repeat
 match goal with
 [ |- context[sqrt ?X] ] ⇒ set (sqrt X)
 end.

Ltac study := red;simpl;unfold_all;field_simplify;[(repeat (rewrite sqrt_pow));set_all_sqrt|..].

Ltac prepare_trans := unfold is_ceva_conjugate, is_cross_sum, is_cross_point, eq_points, ceva_conjugate;
simpl;split.

Ltac solve_trans := intros;prepare_trans;solve_eq.